$\forall$$A$:Type, ${\it eq}$:EqDecider($A$), $B$:($A$$\rightarrow$Type), $P$:($A$$\rightarrow\mathbb{B}$), $f$:$x$:$A$ fp$\rightarrow$ $B$($x$), $a$:$A$.
\\[0ex]$a$ $\in$ dom($f$) $\Rightarrow$ ($\forall$$b$:$A$. $P$($b$) $\Leftrightarrow$ $b$ $=$ $a$) $\Rightarrow$ fpf{-}vals(${\it eq}$;$P$;$f$) $=$ [$\langle$$a$$,\,$$f$($a$)$\rangle$] $\in$ ($x$:$A$$\times$$B$($x$)) List